Search Results

Documents authored by Goranko, Valentin

Document
DOI: 10.4230/LIPIcs.FSCD.2023.23
Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach

Authors: Serenella Cerrito, Valentin Goranko, and Sophie Paillocher

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.
Cite as

Serenella Cerrito, Valentin Goranko, and Sophie Paillocher. Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cerrito_et_al:LIPIcs.FSCD.2023.23,
  author =	{Cerrito, Serenella and Goranko, Valentin and Paillocher, Sophie},
  title =	{{Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.23},
  URN =		{urn:nbn:de:0030-drops-180075},
  doi =		{10.4230/LIPIcs.FSCD.2023.23},
  annote =	{Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.13
Minimisation of Models Satisfying CTL Formulas

Authors: Serenella Cerrito, Amélie David, and Valentin Goranko

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.
Cite as

Serenella Cerrito, Amélie David, and Valentin Goranko. Minimisation of Models Satisfying CTL Formulas. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{cerrito_et_al:LIPIcs.TIME.2019.13,
  author =	{Cerrito, Serenella and David, Am\'{e}lie and Goranko, Valentin},
  title =	{{Minimisation of Models Satisfying CTL Formulas}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.13},
  URN =		{urn:nbn:de:0030-drops-113718},
  doi =		{10.4230/LIPIcs.TIME.2019.13},
  annote =	{Keywords: CTL, model minimisation, bisimulation reduction, tableaux-based reduction}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.14
CTL with Finitely Bounded Semantics

Authors: Valentin Goranko, Antti Kuusisto, and Raine Rönnholm

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.
Cite as

Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{goranko_et_al:LIPIcs.TIME.2017.14,
  author =	{Goranko, Valentin and Kuusisto, Antti and R\"{o}nnholm, Raine},
  title =	{{CTL with Finitely Bounded Semantics}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.14},
  URN =		{urn:nbn:de:0030-drops-79325},
  doi =		{10.4230/LIPIcs.TIME.2017.14},
  annote =	{Keywords: CTL, finitely bounded semantics, tableaux, decidability}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2017
LIPIcs, Volume 82, CSL'17, Complete Volume

Authors: Valentin Goranko and Mads Dam

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
LIPIcs, Volume 82, CSL'17, Complete Volume
Cite as

26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{goranko_et_al:LIPIcs.CSL.2017,
  title =	{{LIPIcs, Volume 82, CSL'17, Complete Volume}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017},
  URN =		{urn:nbn:de:0030-drops-78103},
  doi =		{10.4230/LIPIcs.CSL.2017},
  annote =	{Keywords: Conference Proceedings, Software/Program Verification, Formal Definitions and Theory, Language Constructs and Features, Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2017.0
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Valentin Goranko and Mads Dam

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as

26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{goranko_et_al:LIPIcs.CSL.2017.0,
  author =	{Goranko, Valentin and Dam, Mads},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.0},
  URN =		{urn:nbn:de:0030-drops-76671},
  doi =		{10.4230/LIPIcs.CSL.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact